Symbolic execution combines explicit exploration of every feasible execution path of a computer program with a symbolic representation of input values. Symbols are injected instead of input values, where a symbol represents any value in the corresponding domain. Using the symbolic values, properties relating to every potential execution of the execution path may be analyzed. For example, absence of failures on all possible inputs that lead the program through this execution path may be determined or a counter-example may be provided to demonstrate such failure.
Symbolic execution can be implemented in a variety of manners. In one implementation, the computer program is compiled to create an executable file which is configured to perform the symbolic execution when executed. In an alternative implementation, an interpreter is used to interpret the computer program and simulate symbolic execution thereof. In the present disclosure, “symbolic execution” covers both these implementations, as well as any other implementation.
Symbolic execution, however, suffers from a drawback known as path explosion. As each execution path of the program is traversed, symbolic execution may not be feasible when there are many execution paths that need to be traversed. Such may be the case when, during execution, there is a sequence of branches each of which spawns more than one feasible sub-path, thereby increasing the number of the total paths exponentially in the number of branches.